Iof proof for Lemma comp nat ind tp:
1. P :
{k}
2.
i:. (j:. (j < i) 
P(j)) P(i)
zz,i:. (i < zz) P(i)
by D 0
1:
1: 3. zz :
1: i:. (i < zz) P(i)
2: .....wf..... NILNIL
2: 
Type
.| 9,38 |
{k}
i:. (j:. (j < i) P(j)) P(i)
zz,i:. (i < zz) P(i)
by D 0
1:
1: 3. zz :
1: i:. (i < zz) P(i)
2: .....wf..... NILNIL
2: Type
.
| Definitions | x:A. B(x) T |
| Lemmas |